Łukasiewicz Propositional logic
#古典的命題論理　
#構文論(古典的命題論理)
以下LP
次の言語が必要
要素命題記号
$ p_1 \cdots p_{n}
結合子
$ \lnot, \to
括弧
$ (,)
論理式の定義
1. 単一の要素命題記号
2. 論理式$ Aについて$ (\lnot A)
3. 論理式$ A,Bについて$ (A \to B)
4. 1~3のみを論理式とする
省略のために
$ A \lor Bを$ \lnot A \to Bの省略とする
$ A \land Bは$ \lnot (A \to \lnot B)の省略
$ A \equiv Bは$ (A \to B) \land (B \to A)の省略
Łukasiewiczの3公理図式
1. $ A \to (B \to C) ，以下$ L_1
2. $ (A \to (B \to C)) \to ((A \to B) \to (A \to C))，以下$ L_2
3. $ (\lnot B \to \lnot A) \to (A \to B)，以下$ L_3
推論規則
モーダス・ポネンス
証明 (Łukasiewicz Propositional logic)
「$ A_{1} \cdots A_{n}」が「$ B」のLPにおいての証明であるとは
$ A_{n}は$ Bであって，任意の$ i = 1, 2 \cdots nにおいて次のどちらかである
1. $ A_iは公理である
2. $ j, k < iについて$ A_{i}が$ A_{j}, A_{k}のモーダス・ポネンスによって導出される
更に簡単のために
「$ A_{1} \cdots A_{n}」が「前提$ X_1 \cdots X_{n}から導出される$ B」のLPにおいての証明であるとは
$ A_{n}は$ Bであって，任意の$ i = 1, 2 \cdots nにおいて次のどちらかである
1. $ A_iはŁukasiewiczの3公理図式または$ X_{1} \cdots X_{n}のどれかである
2. $ j, k < iについて$ A_{i}が$ A_{j}, A_{k}のモーダス・ポネンスによって導出される
「$ X_{1} \cdots X_{n} \vdash B」と書く
構文論的演繹定理
$ A_1 \cdots A_{n-1}, A_n \vdash B \implies A_1 \cdots A_{n-1} \vdash A_n \to B
これはNatural-rule Systemの$ \to\text{後}でもあると言える
$ A,\Gamma \to B \implies \Gamma \to (A \to B)
派生的推論規則
論理式$ A,Bについて
$ \lnot B \to \lnot A \vdash A \to Bから，
$ \lnot B \to \lnot A \implies A \to Bという派生的推論規則を使用可能
$ A \to B, B \to C \vdash A \to Cから
$ A \to B, B \to C \implies A \to Cという派生的推論規則（シロギズム）を使用可能
今，Natural-rule Systemの各規則を頑張ってLPの規則で翻訳する
生成規則
$ \land\text{前}:$ A \land B \implies A，$ A \land B \implies B
$ \lnot (A \to \lnot B) \implies A
$ \lnot (A \to \lnot B) \implies B
$ \land\text{後}: $ A,B \implies A \land B
$ A,B \implies \lnot (A \to \lnot B)
$ \lor{後}:$ A \implies A \lor Bまたは$ A \implies B \lor A
$ A \to \lnot A \to B
$ A \to \lnot B \to A
$ \to\text{前}(モーダス・ポネンス): $ A \to B, A \implies B
推論規則そのまま
$ \lnot\text{前}: $ A, \lnot A \implies \bot
$ A, \lnot A \implies p_1 \land \lnot p_1
$ \bot: $ \bot \implies X
$ p_1 \land \lnot p_1 \implies X
二重否定: $ \lnot\lnot A \implies A
そのまま
証明構造に関する規則
$ \to\text{後}:$ A, \Gamma \to B \implies \Gamma \to (A \to B)
構文論的演繹定理
$ \lnot\text{後}: $ A, \Gamma \to \bot \implies \Gamma \to \lnot A
$ A_1 \cdots A_{n-1}, A_{n} \vdash p_1 \land \lnot p_1ならば$ A_1 \cdots A_{n-1} \vdash \lnot A_{n}
$ \lor{前}: $ (A,\Gamma_1 \to C), (B,\Gamma_2 \to C) \implies (\Gamma_1, \Gamma_2) \to (A \lor B \to C)
$ A_1 \cdots A_{n-1}, A_{n} \vdash Cかつ$ B_1 \cdots B_{m-1}, B_{m} \vdash Cならば$ A_{1} \cdots A_{n-1}, B_1, \cdots B_{m-1}, A \lor B \vdash C
これらの翻訳は次の6個の論理式が証明されていると導き出すことが出来る，$ A,Bは任意の論理式
1. $ \lnot A \to (A \to B)
爆発律，つまり矛盾からは任意の論理式を作り出すことが出来る
2. $ \lnot\lnot A \to A
3. $ A \to \lnot\lnot A
4. $ (A \to B) \to (\lnot B \to \lnot A)
5. $ A \to (\lnot\lnot B \to \lnot(A \to \lnot B))
6. $ (A \to B) \to ((\lnot A \to B) \to B)
結論として，Natural-rule Systemでの証明はŁukasiewicz Propositional logicでの証明に変換可能(古典的命題論理)
完全性定理(古典的命題論理)のための
論理式
$ ((B \to \lnot A) \land (C \to A)) \to \lnot(B \land C)
推論
$ B \to \lnot A, C \to A \implies \lnot(B \land C)
$ \lnot\lnot (B \to \lnot A), \lnot\lnot( C \to \lnot\lnot A )\implies \lnot(B \land C)
$ \lnot(B \land A), \lnot(C \land \lnot A) \implies \lnot (B \land C)
$ Bが$ Aの否定を導出して，$ Cが$ Aを導出するなら，$ Bと$ Cは同時に成立しない
これは簡単のためにNRPから証明できて，つまりLPでも証明出来る
重要な事実
LPから導出される論理式はトートロジー(古典的命題論理)のみで，矛盾を導出しない
$ \vDash Aならば$ \vdash A（LPは全てのトートロジーを証明する）
$ \vdash Aならば$ \vDash A（LPが証明する論理式は全てトートロジーである）